$\forall$$M$, $A$:MsgA, $k$:Knd, $l$:IdLnk, ${\it tfL}$:(${\it tg}$:Id$\times$($A$.state$\rightarrow$$A$.da($k$)$\rightarrow$($A$.dout($l$,${\it tg}$) List))) List.
\\[0ex]$M$.rframe($A$.sends ${\it tfL}$ of $k$ on $l$) $\in$ Prop